Nuprl Definition : int_loset
13,42
postcript
pdf
int_loset() == mk_oset(
;
x
,
y
. (
x
=
y
);
x
,
y
.
x
z
y
)
latex
Up
sets
1
Wellformedness Lemmas
int
loset
wf
Definitions
mk_oset(
T
;
eq
;
leq
)
,
(
i
=
j
)
,
i
z
j
origin
;
x,y. (x =
y);x,y. x 
z y) ;x,y. (x = y);x,y. x z y) j)z j